|
| 1: |
|
p(s(N)) |
→ N |
| 2: |
|
N + 0 |
→ N |
| 3: |
|
s(N) + s(M) |
→ s(s(N + M)) |
| 4: |
|
N * 0 |
→ 0 |
| 5: |
|
s(N) * s(M) |
→ s(N + (M + (N * M))) |
| 6: |
|
gt(0,M) |
→ False |
| 7: |
|
gt(NzN,0) |
→ u_4(is_NzNat(NzN)) |
| 8: |
|
u_4(True) |
→ True |
| 9: |
|
is_NzNat(0) |
→ False |
| 10: |
|
is_NzNat(s(N)) |
→ True |
| 11: |
|
gt(s(N),s(M)) |
→ gt(N,M) |
| 12: |
|
lt(N,M) |
→ gt(M,N) |
| 13: |
|
d(0,N) |
→ N |
| 14: |
|
d(s(N),s(M)) |
→ d(N,M) |
| 15: |
|
quot(N,NzM) |
→ u_11(is_NzNat(NzM),N,NzM) |
| 16: |
|
u_11(True,N,NzM) |
→ u_1(gt(N,NzM),N,NzM) |
| 17: |
|
u_1(True,N,NzM) |
→ s(quot(d(N,NzM),NzM)) |
| 18: |
|
quot(NzM,NzM) |
→ u_01(is_NzNat(NzM)) |
| 19: |
|
u_01(True) |
→ s(0) |
| 20: |
|
quot(N,NzM) |
→ u_21(is_NzNat(NzM),NzM,N) |
| 21: |
|
u_21(True,NzM,N) |
→ u_2(gt(NzM,N)) |
| 22: |
|
u_2(True) |
→ 0 |
| 23: |
|
gcd(0,N) |
→ 0 |
| 24: |
|
gcd(NzM,NzM) |
→ u_02(is_NzNat(NzM),NzM) |
| 25: |
|
u_02(True,NzM) |
→ NzM |
| 26: |
|
gcd(NzN,NzM) |
→ u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM) |
| 27: |
|
u_31(True,True,NzN,NzM) |
→ u_3(gt(NzN,NzM),NzN,NzM) |
| 28: |
|
u_3(True,NzN,NzM) |
→ gcd(d(NzN,NzM),NzM) |
|
There are 29 dependency pairs:
|
| 29: |
|
s(N) +# s(M) |
→ N +# M |
| 30: |
|
s(N) *# s(M) |
→ N +# (M + (N * M)) |
| 31: |
|
s(N) *# s(M) |
→ M +# (N * M) |
| 32: |
|
s(N) *# s(M) |
→ N *# M |
| 33: |
|
GT(NzN,0) |
→ U_4(is_NzNat(NzN)) |
| 34: |
|
GT(NzN,0) |
→ IS_NZNAT(NzN) |
| 35: |
|
GT(s(N),s(M)) |
→ GT(N,M) |
| 36: |
|
LT(N,M) |
→ GT(M,N) |
| 37: |
|
D(s(N),s(M)) |
→ D(N,M) |
| 38: |
|
QUOT(N,NzM) |
→ U_11(is_NzNat(NzM),N,NzM) |
| 39: |
|
U_11(True,N,NzM) |
→ U_1(gt(N,NzM),N,NzM) |
| 40: |
|
U_11(True,N,NzM) |
→ GT(N,NzM) |
| 41: |
|
U_1(True,N,NzM) |
→ QUOT(d(N,NzM),NzM) |
| 42: |
|
U_1(True,N,NzM) |
→ D(N,NzM) |
| 43: |
|
QUOT(NzM,NzM) |
→ U_01(is_NzNat(NzM)) |
| 44: |
|
QUOT(NzM,NzM) |
→ IS_NZNAT(NzM) |
| 45: |
|
QUOT(N,NzM) |
→ U_21(is_NzNat(NzM),NzM,N) |
| 46: |
|
QUOT(N,NzM) |
→ IS_NZNAT(NzM) |
| 47: |
|
U_21(True,NzM,N) |
→ U_2(gt(NzM,N)) |
| 48: |
|
U_21(True,NzM,N) |
→ GT(NzM,N) |
| 49: |
|
GCD(NzM,NzM) |
→ U_02(is_NzNat(NzM),NzM) |
| 50: |
|
GCD(NzM,NzM) |
→ IS_NZNAT(NzM) |
| 51: |
|
GCD(NzN,NzM) |
→ U_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM) |
| 52: |
|
GCD(NzN,NzM) |
→ IS_NZNAT(NzN) |
| 53: |
|
GCD(NzN,NzM) |
→ IS_NZNAT(NzM) |
| 54: |
|
U_31(True,True,NzN,NzM) |
→ U_3(gt(NzN,NzM),NzN,NzM) |
| 55: |
|
U_31(True,True,NzN,NzM) |
→ GT(NzN,NzM) |
| 56: |
|
U_3(True,NzN,NzM) |
→ GCD(d(NzN,NzM),NzM) |
| 57: |
|
U_3(True,NzN,NzM) |
→ D(NzN,NzM) |
|
The approximated dependency graph contains 6 SCCs:
{29},
{32},
{37},
{35},
{38,39,41}
and {51,54,56}.